Логіка в інформатиці
Логіка в інформатиці — це напрям досліджень та галузей знань, де логіка застосовується в інформатиці та штучному інтелекті. Використання логіки дуже ефективне в цих областях''Halpern J.Y., Harper R., Immerman N., Kolaitis Ph.G., Vardi M.Y., and Vianu V.'' On the unususal effectiveness of logic in computer science. — January, 2001.. Область застосування Включаються такі основні застосування: * дослідження в логіці, викликані розвитком комп'ютерних наук. Наприклад, аплікативні обчислювальні системи, теорія обчислень і моделі обчислень; * формальні методи і логіка міркування про поняття. Наприклад, семантична мережаRoussopoulos N.D. A semantic network model of data bases. — TR No 104, Department of Computer Science, University of Toronto, 1976., семантична павутина; * булева логіка і алгебра для розробки апаратного забезпечення комп'ютерів; * розв'язання задач і структурне програмування для розробки прикладних програм і створення складних систем програмного забезпечення * доказове програмування — технологія розробки алгоритмів і програм із доказами правильності алгоритмів; * фундаментальні поняття і уявлення для комп'ютерних наук, які є природною областю для формальної логіки. Наприклад, семантика мов програмуванняScott D.S. The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp.~311-372.; * логіка знань і припущень. Наприклад, штучний інтелект; * мова Пролог і логічне програмування для створення баз знань та експертних систем і досліджень у сфері штучного інтелекту; * логіка для опису просторового положення і переміщення; * логіка в інформаційних технологіях. Наприклад, реляційна модель даних, реляційні СКБД, реляційна алгебра, реляційне числення''Codd E. F.'' Relational Completeness of Data Base Sublanguages. In: R. Rustin (ed.): Database Systems: 65-98, Prentice Hall and IBM Research Report RJ 987, San Jose, California, 1972.; * логіка обчислень з об'єктами. Наприклад, комбінаторна логіка, суперкомбінатори''Peyton Jones S., Eber J.-M., Seward J.'' Composing contracts: an adventure in financial engineering. — ICFP 2000; * логіка для компілювання програмного коду та його оптимізації. Наприклад, категоріальна абстрактна машина; * логіка для еквівалентного перетворення об'єктів. Наприклад, лямбда-числення; * перевиклад логіки і математики в термінах, зрозумілих фахівцям в комп'ютерних наукахAsperti A, and Longo G. Categories, Types and Structures. Category Theory for the working computer scientist. — M.I.T. Press, 1991 (pp. 1-300) . Цей список продовжує поповнюватися. Ефективність логіки в комп'ютерних науках На відміну від природничих наук, комп'ютерні науки отримали великий стимул від широкої і безперервної взаємодії з логікою. Особливу роль у комп'ютерних науках відіграють доказові методи розробки алгоритмів і програм з доказами їхньої правильності. Тестування програм може виявити наявність помилок у програмах, але не може гарантувати їх відсутність. Гарантії відсутності помилок в алгоритмах і програмах можуть дати тільки докази їх правильності. Алгоритм не містить помилок, якщо він дає правильні розв'язки для всіх допустимих даних. Серйозною проблемою для комп'ютерних наук та інформатики є наявність помилок в алгоритмах і програмах, що публікуються в підручниках і навчальних посібниках, а також невміння викладачів і вчителів інформатики виявляти і виправляти помилки в алгоритмах і програмах, складених учнями. Єдиний шлях для подолання цих проблем-це вивчення систематичних методів складання алгоритмів і програм з одночасним аналізом їх правильності в рамках доказового програмування з самого початку навчання основам алгоритмізації і програмування. Складність для викладачів і програмістів полягає в тому, що вони повинні вміти писати не тільки алгоритми і програми, а й докази правильності своїх алгоритмів і програм. На жаль, зараз це не вміють робити ні математики, ні програмісти. В результаті програмісти пишуть програми з великим числом помилок, які вони не можуть ні виявити, ні виправити. Масоване тестування програм на ЕОМ приносить програмістам безперечну користь, проте не дає гарантій повного позбавлення від помилок. Практика застосування та вивчення доказових методів програмування показала, що ця технологія цілком доступна студентам математичних факультетів, яким цілком під силу написання доказів правильності алгоритмів, після перевірки та тестування програм на ЕОМ. Найбільший ефект в освоєнні технологій доказового програмування спостерігається в олімпіадах з інформатики та програмування, де переможцями та призерами стають ті студенти, які освоїли техніку тестування програм на ЕОМ і складання алгоритмів і програм без помилок. Див. також * Програмування * Парадигма програмування * Структурне програмування * Логічне програмування * Інформатика * Комбінаторна логіка * Розв'язання задач * Доказове програмування Посилання Література * Вольфенгаген В. Э. Логика. Конспект лекций: техника рассуждений. 2-е изд., дополн. и перераб. — М: АО «Центр ЮрИнфоР», 2004. — 229 с ISBN 5-89158-135-3. Категорія:Інформатика Категорія:Логіка Категорія:Формальні методи